a mod n == if 0 z a then a rem n if ((-a) rem n = 0) then 0 else n - ((-a) rem n) fi  

latex

Up	int 2, int 2
Wellformedness Lemmas	modulus wf, modulus wf
Definitions	i z j, if b then t else f fi , (i = j), #$n, n - m, n rem m, -n
FDL editor aliases	modulus